plus2(0, x) -> x
plus2(s1(x), y) -> s1(plus2(p1(s1(x)), y))
times2(0, y) -> 0
times2(s1(x), y) -> plus2(y, times2(p1(s1(x)), y))
p1(s1(0)) -> 0
p1(s1(s1(x))) -> s1(p1(s1(x)))
fac2(0, x) -> x
fac2(s1(x), y) -> fac2(p1(s1(x)), times2(s1(x), y))
factorial1(x) -> fac2(x, s1(0))
↳ QTRS
↳ DependencyPairsProof
plus2(0, x) -> x
plus2(s1(x), y) -> s1(plus2(p1(s1(x)), y))
times2(0, y) -> 0
times2(s1(x), y) -> plus2(y, times2(p1(s1(x)), y))
p1(s1(0)) -> 0
p1(s1(s1(x))) -> s1(p1(s1(x)))
fac2(0, x) -> x
fac2(s1(x), y) -> fac2(p1(s1(x)), times2(s1(x), y))
factorial1(x) -> fac2(x, s1(0))
FAC2(s1(x), y) -> FAC2(p1(s1(x)), times2(s1(x), y))
PLUS2(s1(x), y) -> PLUS2(p1(s1(x)), y)
PLUS2(s1(x), y) -> P1(s1(x))
P1(s1(s1(x))) -> P1(s1(x))
TIMES2(s1(x), y) -> TIMES2(p1(s1(x)), y)
TIMES2(s1(x), y) -> P1(s1(x))
FACTORIAL1(x) -> FAC2(x, s1(0))
FAC2(s1(x), y) -> P1(s1(x))
FAC2(s1(x), y) -> TIMES2(s1(x), y)
TIMES2(s1(x), y) -> PLUS2(y, times2(p1(s1(x)), y))
plus2(0, x) -> x
plus2(s1(x), y) -> s1(plus2(p1(s1(x)), y))
times2(0, y) -> 0
times2(s1(x), y) -> plus2(y, times2(p1(s1(x)), y))
p1(s1(0)) -> 0
p1(s1(s1(x))) -> s1(p1(s1(x)))
fac2(0, x) -> x
fac2(s1(x), y) -> fac2(p1(s1(x)), times2(s1(x), y))
factorial1(x) -> fac2(x, s1(0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
FAC2(s1(x), y) -> FAC2(p1(s1(x)), times2(s1(x), y))
PLUS2(s1(x), y) -> PLUS2(p1(s1(x)), y)
PLUS2(s1(x), y) -> P1(s1(x))
P1(s1(s1(x))) -> P1(s1(x))
TIMES2(s1(x), y) -> TIMES2(p1(s1(x)), y)
TIMES2(s1(x), y) -> P1(s1(x))
FACTORIAL1(x) -> FAC2(x, s1(0))
FAC2(s1(x), y) -> P1(s1(x))
FAC2(s1(x), y) -> TIMES2(s1(x), y)
TIMES2(s1(x), y) -> PLUS2(y, times2(p1(s1(x)), y))
plus2(0, x) -> x
plus2(s1(x), y) -> s1(plus2(p1(s1(x)), y))
times2(0, y) -> 0
times2(s1(x), y) -> plus2(y, times2(p1(s1(x)), y))
p1(s1(0)) -> 0
p1(s1(s1(x))) -> s1(p1(s1(x)))
fac2(0, x) -> x
fac2(s1(x), y) -> fac2(p1(s1(x)), times2(s1(x), y))
factorial1(x) -> fac2(x, s1(0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
P1(s1(s1(x))) -> P1(s1(x))
plus2(0, x) -> x
plus2(s1(x), y) -> s1(plus2(p1(s1(x)), y))
times2(0, y) -> 0
times2(s1(x), y) -> plus2(y, times2(p1(s1(x)), y))
p1(s1(0)) -> 0
p1(s1(s1(x))) -> s1(p1(s1(x)))
fac2(0, x) -> x
fac2(s1(x), y) -> fac2(p1(s1(x)), times2(s1(x), y))
factorial1(x) -> fac2(x, s1(0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P1(s1(s1(x))) -> P1(s1(x))
POL(P1(x1)) = 2·x1
POL(s1(x1)) = 1 + 2·x1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
plus2(0, x) -> x
plus2(s1(x), y) -> s1(plus2(p1(s1(x)), y))
times2(0, y) -> 0
times2(s1(x), y) -> plus2(y, times2(p1(s1(x)), y))
p1(s1(0)) -> 0
p1(s1(s1(x))) -> s1(p1(s1(x)))
fac2(0, x) -> x
fac2(s1(x), y) -> fac2(p1(s1(x)), times2(s1(x), y))
factorial1(x) -> fac2(x, s1(0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
PLUS2(s1(x), y) -> PLUS2(p1(s1(x)), y)
plus2(0, x) -> x
plus2(s1(x), y) -> s1(plus2(p1(s1(x)), y))
times2(0, y) -> 0
times2(s1(x), y) -> plus2(y, times2(p1(s1(x)), y))
p1(s1(0)) -> 0
p1(s1(s1(x))) -> s1(p1(s1(x)))
fac2(0, x) -> x
fac2(s1(x), y) -> fac2(p1(s1(x)), times2(s1(x), y))
factorial1(x) -> fac2(x, s1(0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
TIMES2(s1(x), y) -> TIMES2(p1(s1(x)), y)
plus2(0, x) -> x
plus2(s1(x), y) -> s1(plus2(p1(s1(x)), y))
times2(0, y) -> 0
times2(s1(x), y) -> plus2(y, times2(p1(s1(x)), y))
p1(s1(0)) -> 0
p1(s1(s1(x))) -> s1(p1(s1(x)))
fac2(0, x) -> x
fac2(s1(x), y) -> fac2(p1(s1(x)), times2(s1(x), y))
factorial1(x) -> fac2(x, s1(0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
FAC2(s1(x), y) -> FAC2(p1(s1(x)), times2(s1(x), y))
plus2(0, x) -> x
plus2(s1(x), y) -> s1(plus2(p1(s1(x)), y))
times2(0, y) -> 0
times2(s1(x), y) -> plus2(y, times2(p1(s1(x)), y))
p1(s1(0)) -> 0
p1(s1(s1(x))) -> s1(p1(s1(x)))
fac2(0, x) -> x
fac2(s1(x), y) -> fac2(p1(s1(x)), times2(s1(x), y))
factorial1(x) -> fac2(x, s1(0))